#pragma once

#include "henry.hpp"
#include "knowledge_base.hpp"
#include "variable_manager.hpp"

#define INPUT_ERROR_PROBLEM_NOT_FOUND 1
#define INPUT_ERROR_SYNTAX            2

#define LMAX( _h1, _h2, _vec ) (_vec[_h1].number == _vec[_h2].number ? (_h1 < _h2 ? _vec[_h1] : _vec[_h2]) : ( _vec[_h1].number > _vec[_h2].number ? _vec[_h1] : _vec[_h2]))
#define LMIN( _h1, _h2, _vec ) (_vec[_h1].number == _vec[_h2].number ? (_h1 < _h2 ? _vec[_h2] : _vec[_h1]) : ( _vec[_h1].number > _vec[_h2].number ? _vec[_h2] : _vec[_h1]))

using namespace std;

namespace plugin {
  class callback_t; class xor_constraint_t; class conditional_unification_t;
  class prohibit_same_multiple_explanations_t; class prohibit_circular_zero_t;
}

namespace ie {

  struct cluster_t {
    
    int                  num_clusters;
    logvar_set_t         variables;
    unordered_set<int>   unifiers;
    
  };
  
  typedef ss_dict_t input_t;
  
  class variable_cluster_t {

  public:
    typedef unordered_map<int, cluster_t> cluster_set_t;

    struct baby_cluster_t {
      logvar_list_t        variables;
      int_list_t           unifiers;
      int_list_t           links;
      
      baby_cluster_t( const logical_variable_t &v1, const logical_variable_t &v2, int unifier ) {
        variables.push_back( v1 ); variables.push_back( v2 ); unifiers.push_back( unifier );
      }
    };
    
  private:
    vector<baby_cluster_t>                  m_c2v;
    unordered_map<logical_variable_t, int>  m_v2c, m_v2c_flushed;
    
  public:
    inline void del_unifier( const unifier_t &u ) {
      foreach( vector<baby_cluster_t>, iter_c2v, m_c2v ) {
        int_list_t::iterator iter_u = find( iter_c2v->unifiers.begin(), iter_c2v->unifiers.end(), u.id );
        if( iter_c2v->unifiers.end() != iter_u ) { iter_c2v->unifiers.erase( iter_u ); break; }
      }
    }
    
    inline int add_unifier( unifier_t** p_out, const logical_variable_t& v1, const logical_variable_t& v2 ) {
      m_unifier_storage.push_back( unifier_t(v1, v2) );
      int the_passport = m_unifier_storage.size()-1;
      unifier_t *p_unifier = &m_unifier_storage[ the_passport ];
      p_unifier->id = the_passport;
      
      if( NULL != p_out ) *p_out = p_unifier;
      
      unordered_map<logical_variable_t, int>::iterator iter_v1 = m_v2c.find( v1 ), iter_v2 = m_v2c.find( v2 );
      
      if( m_v2c.end() == iter_v1 && m_v2c.end() == iter_v2 ) {

        /* Create new cluster. */
        baby_cluster_t bc( v1, v2, the_passport );
        m_c2v.push_back( bc );
        
        m_v2c[ v1 ] = m_c2v.size()-1; m_v2c[ v2 ] = m_c2v.size()-1;
        
      } else if( m_v2c.end() != iter_v1 && m_v2c.end() != iter_v2 ) {

        if( iter_v1->second == iter_v2->second ) {
          m_c2v[ iter_v1->second ].unifiers.push_back( the_passport );
          return the_passport;
        }

        /* Link these clusters. */
        m_c2v[ iter_v1->second ].links.push_back( iter_v2->second );
        m_c2v[ iter_v2->second ].links.push_back( iter_v1->second );
        m_c2v[ iter_v1->second ].unifiers.push_back( the_passport );
        m_c2v[ iter_v2->second ].unifiers.push_back( the_passport );

      } else {

        /* Follow each other. */
        if( m_v2c.end() == iter_v2 ) { m_v2c[ v2 ] = iter_v1->second; m_c2v[ iter_v1->second ].variables.push_back( v2 ); m_c2v[ iter_v1->second ].unifiers.push_back( the_passport ); }
        else                         { m_v2c[ v1 ] = iter_v2->second; m_c2v[ iter_v2->second ].variables.push_back( v1 ); m_c2v[ iter_v2->second ].unifiers.push_back( the_passport ); }
        
      }
      return the_passport;
    }
    
    cluster_set_t                          m_cluster_set;
    vector<unifier_t>                      m_unifier_storage;
    
  public:
    variable_cluster_t() {};
    ~variable_cluster_t() {};
    
    void flush();

    inline unifier_t *get_unifier( int u ) { return &m_unifier_storage[u]; }
    inline unifier_t *get_unifier_storage() { return &m_unifier_storage[0]; }
    inline cluster_set_t &get_cluster_set() { return m_cluster_set; };

    inline int get_raw_cluster_variables( logvar_list_t *p_out, const logical_variable_t &v ) { p_out->push_back( v ); int c = get_raw_cluster_id( v ); if( -1 == c ) { return -1; } p_out->insert( p_out->end(), m_c2v[c].variables.begin(), m_c2v[c].variables.end() ); return c; }
    inline int get_raw_cluster_id( const logical_variable_t &v ) { vi_dict_t::const_iterator iter_v = m_v2c.find( v ); return m_v2c.end() == iter_v ? -1 : iter_v->second; };
    inline int get_cluster_id( const logical_variable_t &v ) { vi_dict_t::const_iterator iter_v = m_v2c_flushed.find( v ); return m_v2c_flushed.end() == iter_v ? -1 : iter_v->second; };
    
    bool is_in_same_cluster( const logical_variable_t &v1, const logical_variable_t &v2 ) {
      unordered_map<logical_variable_t,int>::iterator c1 = m_v2c_flushed.find( v1 ), c2 = m_v2c_flushed.find( v2 );
      return ( m_v2c_flushed.end() == c1 || m_v2c_flushed.end() == c2 ) ? false : c1->second == c2->second;
    }
    
  };

  typedef unordered_map<logical_variable_t, sil_dict_t > var_hypo_dict_t;
  typedef unordered_map<string, ilp::variable_t>       e_dict_t;
  typedef unordered_map<string, vector<int> >           eu_dict_t;
  typedef unordered_map<int, ilp::variable_t>          cx_dict_t;
  typedef unordered_map<logical_variable_t, cx_dict_t> var_cx_dict_t;
  typedef unordered_map<string, unordered_map<logical_variable_t, int_list_t> > attr_var_dict_t;
  typedef unordered_map<ilp::variable_t,pair<ilp::constraint_t,vector<ilp::variable_set_t> > > u2e_dict_t;
  typedef unordered_map<string, vector<unifier_operator_t*> > unifiable_dict_t;
  
  class weighted_abduction_t {

    friend class plugin::callback_t;
    friend class plugin::xor_constraint_t;
    friend class plugin::conditional_unification_t;
    friend class plugin::prohibit_same_multiple_explanations_t;
    friend class plugin::prohibit_circular_zero_t;
    
  private:
   
    kb::pool_t             *m_p_kbp;
    ilp::solver_t           m_ilp_solver;
    literal_vector_t        m_hypotheses;
    unified_literal_dict_t  m_unified;
    list<unifier_t>         m_inequalities;
    list<unifier_t>         m_unifier_storage;
    variable_manager_t      m_vm;
    variable_cluster_t      m_vc;
    vs_dict_t               m_v2c;
    sv_dict_t               m_c2n;
    var_hypo_dict_t         m_v2h, m_v2h_o;
    slpl_dict_t             m_pa2h;
    unifiable_dict_t        m_unifiable;
    int_set_t               m_pu_proved_infeasible;
    e_dict_t                m_edict;
    eu_dict_t               m_eudict;
    var_cx_dict_t           m_var_cx;
    vi_dict_t               m_var_vc;
    svset_dict_t            m_c2v;
    u2e_dict_t              m_u2e;
    iiset_dict_t            m_var_deps;
    double                  m_time_prepare, m_time_ilp;
    double                  m_cost, m_initial_cost, m_initial_cost_eps;
    int                     m_num_var_h, m_num_var_r, m_num_var_u, m_num_var_c, m_num_var_e;
    literal_list_t          m_input;
    variable_cluster_t      m_non_merges;
    string_set_t            m_constraints, m_best_axioms;

    /* Options. */
    int      m_depth_limit;
    int      m_recursion_limit;
    bool     m_f_rhs_strict, m_f_expl_mutual_exclusive, m_f_block_multiple_same_explanations;
    bool     m_f_no_group_merge, m_f_use_ilp_heuristics, m_f_diet, m_f_block_circular_zero;
    bool     m_f_bc_from_same_prefix;
    ostream *m_p_ilp_log;
    string   m_problem;
    string   m_command;
    double   m_time_start, m_timeout;

    bool _is_worth_unifying( const literal_t &h1, const literal_t &h2 );
    
    bool _prepare_diet( const vector<int_list_t>& );
    bool _prepare_unification( unordered_map<literal_t*,ilp::variable_set_t>* );
    bool _prepare_reduce_triggers( const unordered_map<literal_t*,ilp::variable_set_t>& );
    bool _prepare_variable_clusters();
    bool _prepare_multiple_rhs();

    
  public:
    weighted_abduction_t( kb::pool_t*, string& );
    ~weighted_abduction_t();

    void del_literal( literal_t* );
    int add_literal( const literal_t&, int = 0 );
    ilp::variable_t add_variable_e( logical_variable_t&, ilp::variable_t, logical_variable_t&, ilp::variable_t, int, int = -1 );
    inline int_list_t &get_eu_dict( const logical_variable_t& v1, const logical_variable_t& v2 ) {
      static char buffer[ 1024 ]; sprintf( buffer, "%s/%s/%d", g_vm.p2v(v1 < v2 ? v1 : v2).c_str(), g_vm.p2v(v1 < v2 ? v2 : v1).c_str(), 0 );
      string ek( buffer );
      return m_eudict[ ek ];
    };
    inline ilp::variable_t find_variable_e( const logical_variable_t& v1, const logical_variable_t& v2, int t ) {
      static char buffer[ 1024 ]; sprintf( buffer, "%s/%s/%d", g_vm.p2v(v1 < v2 ? v1 : v2).c_str(), g_vm.p2v(v1 < v2 ? v2 : v1).c_str(), t );
      string ek( buffer );
      e_dict_t::iterator iter_e = m_edict.find( ek );
      return m_edict.end() == iter_e ? ilp::INVALID_HANDLE : iter_e->second;
    };
    inline ilp::variable_t collect_variable_e( ilp::variable_set_t *p_out, const logical_variable_t& v1, const logical_variable_t& v2 ) {
      for( int i=0; i<9999; i++ ) {
        ilp::variable_t var_e = find_variable_e( v1, v2, i );
        if( ilp::INVALID_HANDLE == var_e ) break;
        p_out->insert( var_e );
      }
    }
    
    bool ready_set( bool = false );
    void go();

    bool reasoning( literal_t&, literal_pset_t*, slps_dict_t&, slpl_dict_t*, siil_dict_t* = NULL, int = -1 );
    
    void draw_graph( ostream&, graph_repr_t );
    void print_observations();
    void print_axioms( bool = false );
    void print_variable_substitutions();
    void print_ilp();
    inline void print_constraints() { cout << "[Constraints Generated by Conditioned Unification]" << endl; foreach( string_set_t, iter_c, m_constraints ) cout << *iter_c << endl; cout << endl; }
    
    inline bool is_timeout() { m_time_prepare = gettimeofday_sec() - m_time_start; return m_time_prepare > m_timeout; };

    inline void set_problem( string &name, literal_list_t &prob ) { m_problem = name; m_input = prob; };
    inline void set_recursion_limit( int rec ) { m_recursion_limit = rec; };
    inline void set_rhs_restrict( bool f_switch ) { m_f_rhs_strict = f_switch; };
    inline void set_expl_mutual_exclusiveness( bool f_switch ) { m_f_expl_mutual_exclusive = f_switch; };
    inline void set_ilp_log( ostream &os ) { m_p_ilp_log = &os; };
    inline void set_ilp_heuristics( bool f_switch ) { m_f_use_ilp_heuristics = f_switch; };
    inline void set_diet_mode( bool f_switch ) { m_f_diet = f_switch; }
    inline void set_block_multiple_explanations( bool f_switch ) { m_f_block_multiple_same_explanations = f_switch; }
    inline void set_block_circular_zero( bool f_switch ) { m_f_block_circular_zero = f_switch; }
    inline void set_bc_from_same_prefix( bool f_switch ) { m_f_bc_from_same_prefix = f_switch; }
    
    inline void set_depth_limit( int _depth ) { m_depth_limit = _depth; };
    inline void set_timeout( double t ) { m_timeout = t; };

    inline literal_vector_t &get_hypotheses() { return m_hypotheses; };
    inline unified_literal_dict_t &get_unify_dict() { return m_unified; };
    inline bool get_rhs_restrict() { return m_f_rhs_strict; };
    inline ilp::solver_t &get_ilp_solver() { return m_ilp_solver; }
    inline variable_cluster_t &get_variable_cluster() { return m_vc; }
    inline variable_cluster_t &get_non_merge_cluster() { return m_non_merges; }
    inline variable_manager_t &get_variable_manager() { return m_vm; }
    
    inline unifier_operator_t *get_unifier_op( int h1, int h2 ) {
      unified_literal_dict_t::iterator iter_first = m_unified.find( h1 );
      if( m_unified.end() != iter_first ) {
        iu_dict_t::iterator iter_second = iter_first->second.find( h2 );
        if( iter_first->second.end() != iter_second ) return &iter_second->second;
      }
      iter_first = m_unified.find( h2 );
      if( m_unified.end() != iter_first ) {
        iu_dict_t::iterator iter_second = iter_first->second.find( h1 );
        if( iter_first->second.end() != iter_second ) return &iter_second->second;
      }
      return NULL;
    }
      
  };
  
  class input_storage_t {
    
  private:
    input_t m_input;
    
  public:
    void load( string_list_t*, istream& );
    int parse_input( literal_list_t*, string& );
    
  };
  
};
